the_es:ES, e', e:E. (e  before(e'))  (e <loc e') 

latex

Definitions	x:A. B(x), b, t  T, A, b, Prop, , first(e), P  Q, P & Q, P  Q, Unit, E, ES, (e <loc e'), P  Q, (x  l), before(e), {T}, x. t(x), WellFnd{i}(A;x,y.R(x;y)), False, P  Q, as @ bs, pred(e)
Lemmas	es-pred wf, es-pred-locl, es-locl-iff, append wf, member append, cons member, iff functionality wrt iff, or functionality wrt iff, false wf, nil member, es-first-implies, es-locl-wellfnd, es-E wf, l member wf, es-before wf, es-locl wf, event system wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-first wf, bool wf, bnot wf, not wf, assert wf